Left Termination of the query pattern goal_in_3(g, a, a) w.r.t. the given Prolog program could successfully be proven:



↳ Prolog
  ↳ PrologToPiTRSProof

Clauses:

goal(A, B, C) :- ','(s2l(A, D), applast(D, B, C)).
applast(L, X, Last) :- ','(append(L, .(X, []), LX), last(Last, LX)).
last(X, .(X, [])).
last(X, .(H, T)) :- last(X, T).
append([], L, L).
append(.(H, L1), L2, .(H, L3)) :- append(L1, L2, L3).
s2l(s(X), .(Y, Xs)) :- s2l(X, Xs).
s2l(0, []).

Queries:

goal(g,a,a).

We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

goal_in(A, B, C) → U1(A, B, C, s2l_in(A, D))
s2l_in(0, []) → s2l_out(0, [])
s2l_in(s(X), .(Y, Xs)) → U7(X, Y, Xs, s2l_in(X, Xs))
U7(X, Y, Xs, s2l_out(X, Xs)) → s2l_out(s(X), .(Y, Xs))
U1(A, B, C, s2l_out(A, D)) → U2(A, B, C, applast_in(D, B, C))
applast_in(L, X, Last) → U3(L, X, Last, append_in(L, .(X, []), LX))
append_in(.(H, L1), L2, .(H, L3)) → U6(H, L1, L2, L3, append_in(L1, L2, L3))
append_in([], L, L) → append_out([], L, L)
U6(H, L1, L2, L3, append_out(L1, L2, L3)) → append_out(.(H, L1), L2, .(H, L3))
U3(L, X, Last, append_out(L, .(X, []), LX)) → U4(L, X, Last, last_in(Last, LX))
last_in(X, .(H, T)) → U5(X, H, T, last_in(X, T))
last_in(X, .(X, [])) → last_out(X, .(X, []))
U5(X, H, T, last_out(X, T)) → last_out(X, .(H, T))
U4(L, X, Last, last_out(Last, LX)) → applast_out(L, X, Last)
U2(A, B, C, applast_out(D, B, C)) → goal_out(A, B, C)

The argument filtering Pi contains the following mapping:
goal_in(x1, x2, x3)  =  goal_in(x1)
U1(x1, x2, x3, x4)  =  U1(x4)
s2l_in(x1, x2)  =  s2l_in(x1)
0  =  0
[]  =  []
s2l_out(x1, x2)  =  s2l_out(x2)
s(x1)  =  s(x1)
.(x1, x2)  =  .(x2)
U7(x1, x2, x3, x4)  =  U7(x4)
U2(x1, x2, x3, x4)  =  U2(x4)
applast_in(x1, x2, x3)  =  applast_in(x1)
U3(x1, x2, x3, x4)  =  U3(x4)
append_in(x1, x2, x3)  =  append_in(x1, x2)
U6(x1, x2, x3, x4, x5)  =  U6(x5)
append_out(x1, x2, x3)  =  append_out(x3)
U4(x1, x2, x3, x4)  =  U4(x4)
last_in(x1, x2)  =  last_in(x2)
U5(x1, x2, x3, x4)  =  U5(x4)
last_out(x1, x2)  =  last_out
applast_out(x1, x2, x3)  =  applast_out
goal_out(x1, x2, x3)  =  goal_out

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

goal_in(A, B, C) → U1(A, B, C, s2l_in(A, D))
s2l_in(0, []) → s2l_out(0, [])
s2l_in(s(X), .(Y, Xs)) → U7(X, Y, Xs, s2l_in(X, Xs))
U7(X, Y, Xs, s2l_out(X, Xs)) → s2l_out(s(X), .(Y, Xs))
U1(A, B, C, s2l_out(A, D)) → U2(A, B, C, applast_in(D, B, C))
applast_in(L, X, Last) → U3(L, X, Last, append_in(L, .(X, []), LX))
append_in(.(H, L1), L2, .(H, L3)) → U6(H, L1, L2, L3, append_in(L1, L2, L3))
append_in([], L, L) → append_out([], L, L)
U6(H, L1, L2, L3, append_out(L1, L2, L3)) → append_out(.(H, L1), L2, .(H, L3))
U3(L, X, Last, append_out(L, .(X, []), LX)) → U4(L, X, Last, last_in(Last, LX))
last_in(X, .(H, T)) → U5(X, H, T, last_in(X, T))
last_in(X, .(X, [])) → last_out(X, .(X, []))
U5(X, H, T, last_out(X, T)) → last_out(X, .(H, T))
U4(L, X, Last, last_out(Last, LX)) → applast_out(L, X, Last)
U2(A, B, C, applast_out(D, B, C)) → goal_out(A, B, C)

The argument filtering Pi contains the following mapping:
goal_in(x1, x2, x3)  =  goal_in(x1)
U1(x1, x2, x3, x4)  =  U1(x4)
s2l_in(x1, x2)  =  s2l_in(x1)
0  =  0
[]  =  []
s2l_out(x1, x2)  =  s2l_out(x2)
s(x1)  =  s(x1)
.(x1, x2)  =  .(x2)
U7(x1, x2, x3, x4)  =  U7(x4)
U2(x1, x2, x3, x4)  =  U2(x4)
applast_in(x1, x2, x3)  =  applast_in(x1)
U3(x1, x2, x3, x4)  =  U3(x4)
append_in(x1, x2, x3)  =  append_in(x1, x2)
U6(x1, x2, x3, x4, x5)  =  U6(x5)
append_out(x1, x2, x3)  =  append_out(x3)
U4(x1, x2, x3, x4)  =  U4(x4)
last_in(x1, x2)  =  last_in(x2)
U5(x1, x2, x3, x4)  =  U5(x4)
last_out(x1, x2)  =  last_out
applast_out(x1, x2, x3)  =  applast_out
goal_out(x1, x2, x3)  =  goal_out


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

GOAL_IN(A, B, C) → U11(A, B, C, s2l_in(A, D))
GOAL_IN(A, B, C) → S2L_IN(A, D)
S2L_IN(s(X), .(Y, Xs)) → U71(X, Y, Xs, s2l_in(X, Xs))
S2L_IN(s(X), .(Y, Xs)) → S2L_IN(X, Xs)
U11(A, B, C, s2l_out(A, D)) → U21(A, B, C, applast_in(D, B, C))
U11(A, B, C, s2l_out(A, D)) → APPLAST_IN(D, B, C)
APPLAST_IN(L, X, Last) → U31(L, X, Last, append_in(L, .(X, []), LX))
APPLAST_IN(L, X, Last) → APPEND_IN(L, .(X, []), LX)
APPEND_IN(.(H, L1), L2, .(H, L3)) → U61(H, L1, L2, L3, append_in(L1, L2, L3))
APPEND_IN(.(H, L1), L2, .(H, L3)) → APPEND_IN(L1, L2, L3)
U31(L, X, Last, append_out(L, .(X, []), LX)) → U41(L, X, Last, last_in(Last, LX))
U31(L, X, Last, append_out(L, .(X, []), LX)) → LAST_IN(Last, LX)
LAST_IN(X, .(H, T)) → U51(X, H, T, last_in(X, T))
LAST_IN(X, .(H, T)) → LAST_IN(X, T)

The TRS R consists of the following rules:

goal_in(A, B, C) → U1(A, B, C, s2l_in(A, D))
s2l_in(0, []) → s2l_out(0, [])
s2l_in(s(X), .(Y, Xs)) → U7(X, Y, Xs, s2l_in(X, Xs))
U7(X, Y, Xs, s2l_out(X, Xs)) → s2l_out(s(X), .(Y, Xs))
U1(A, B, C, s2l_out(A, D)) → U2(A, B, C, applast_in(D, B, C))
applast_in(L, X, Last) → U3(L, X, Last, append_in(L, .(X, []), LX))
append_in(.(H, L1), L2, .(H, L3)) → U6(H, L1, L2, L3, append_in(L1, L2, L3))
append_in([], L, L) → append_out([], L, L)
U6(H, L1, L2, L3, append_out(L1, L2, L3)) → append_out(.(H, L1), L2, .(H, L3))
U3(L, X, Last, append_out(L, .(X, []), LX)) → U4(L, X, Last, last_in(Last, LX))
last_in(X, .(H, T)) → U5(X, H, T, last_in(X, T))
last_in(X, .(X, [])) → last_out(X, .(X, []))
U5(X, H, T, last_out(X, T)) → last_out(X, .(H, T))
U4(L, X, Last, last_out(Last, LX)) → applast_out(L, X, Last)
U2(A, B, C, applast_out(D, B, C)) → goal_out(A, B, C)

The argument filtering Pi contains the following mapping:
goal_in(x1, x2, x3)  =  goal_in(x1)
U1(x1, x2, x3, x4)  =  U1(x4)
s2l_in(x1, x2)  =  s2l_in(x1)
0  =  0
[]  =  []
s2l_out(x1, x2)  =  s2l_out(x2)
s(x1)  =  s(x1)
.(x1, x2)  =  .(x2)
U7(x1, x2, x3, x4)  =  U7(x4)
U2(x1, x2, x3, x4)  =  U2(x4)
applast_in(x1, x2, x3)  =  applast_in(x1)
U3(x1, x2, x3, x4)  =  U3(x4)
append_in(x1, x2, x3)  =  append_in(x1, x2)
U6(x1, x2, x3, x4, x5)  =  U6(x5)
append_out(x1, x2, x3)  =  append_out(x3)
U4(x1, x2, x3, x4)  =  U4(x4)
last_in(x1, x2)  =  last_in(x2)
U5(x1, x2, x3, x4)  =  U5(x4)
last_out(x1, x2)  =  last_out
applast_out(x1, x2, x3)  =  applast_out
goal_out(x1, x2, x3)  =  goal_out
S2L_IN(x1, x2)  =  S2L_IN(x1)
U51(x1, x2, x3, x4)  =  U51(x4)
U31(x1, x2, x3, x4)  =  U31(x4)
LAST_IN(x1, x2)  =  LAST_IN(x2)
U41(x1, x2, x3, x4)  =  U41(x4)
APPLAST_IN(x1, x2, x3)  =  APPLAST_IN(x1)
APPEND_IN(x1, x2, x3)  =  APPEND_IN(x1, x2)
U21(x1, x2, x3, x4)  =  U21(x4)
U61(x1, x2, x3, x4, x5)  =  U61(x5)
U71(x1, x2, x3, x4)  =  U71(x4)
GOAL_IN(x1, x2, x3)  =  GOAL_IN(x1)
U11(x1, x2, x3, x4)  =  U11(x4)

We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

GOAL_IN(A, B, C) → U11(A, B, C, s2l_in(A, D))
GOAL_IN(A, B, C) → S2L_IN(A, D)
S2L_IN(s(X), .(Y, Xs)) → U71(X, Y, Xs, s2l_in(X, Xs))
S2L_IN(s(X), .(Y, Xs)) → S2L_IN(X, Xs)
U11(A, B, C, s2l_out(A, D)) → U21(A, B, C, applast_in(D, B, C))
U11(A, B, C, s2l_out(A, D)) → APPLAST_IN(D, B, C)
APPLAST_IN(L, X, Last) → U31(L, X, Last, append_in(L, .(X, []), LX))
APPLAST_IN(L, X, Last) → APPEND_IN(L, .(X, []), LX)
APPEND_IN(.(H, L1), L2, .(H, L3)) → U61(H, L1, L2, L3, append_in(L1, L2, L3))
APPEND_IN(.(H, L1), L2, .(H, L3)) → APPEND_IN(L1, L2, L3)
U31(L, X, Last, append_out(L, .(X, []), LX)) → U41(L, X, Last, last_in(Last, LX))
U31(L, X, Last, append_out(L, .(X, []), LX)) → LAST_IN(Last, LX)
LAST_IN(X, .(H, T)) → U51(X, H, T, last_in(X, T))
LAST_IN(X, .(H, T)) → LAST_IN(X, T)

The TRS R consists of the following rules:

goal_in(A, B, C) → U1(A, B, C, s2l_in(A, D))
s2l_in(0, []) → s2l_out(0, [])
s2l_in(s(X), .(Y, Xs)) → U7(X, Y, Xs, s2l_in(X, Xs))
U7(X, Y, Xs, s2l_out(X, Xs)) → s2l_out(s(X), .(Y, Xs))
U1(A, B, C, s2l_out(A, D)) → U2(A, B, C, applast_in(D, B, C))
applast_in(L, X, Last) → U3(L, X, Last, append_in(L, .(X, []), LX))
append_in(.(H, L1), L2, .(H, L3)) → U6(H, L1, L2, L3, append_in(L1, L2, L3))
append_in([], L, L) → append_out([], L, L)
U6(H, L1, L2, L3, append_out(L1, L2, L3)) → append_out(.(H, L1), L2, .(H, L3))
U3(L, X, Last, append_out(L, .(X, []), LX)) → U4(L, X, Last, last_in(Last, LX))
last_in(X, .(H, T)) → U5(X, H, T, last_in(X, T))
last_in(X, .(X, [])) → last_out(X, .(X, []))
U5(X, H, T, last_out(X, T)) → last_out(X, .(H, T))
U4(L, X, Last, last_out(Last, LX)) → applast_out(L, X, Last)
U2(A, B, C, applast_out(D, B, C)) → goal_out(A, B, C)

The argument filtering Pi contains the following mapping:
goal_in(x1, x2, x3)  =  goal_in(x1)
U1(x1, x2, x3, x4)  =  U1(x4)
s2l_in(x1, x2)  =  s2l_in(x1)
0  =  0
[]  =  []
s2l_out(x1, x2)  =  s2l_out(x2)
s(x1)  =  s(x1)
.(x1, x2)  =  .(x2)
U7(x1, x2, x3, x4)  =  U7(x4)
U2(x1, x2, x3, x4)  =  U2(x4)
applast_in(x1, x2, x3)  =  applast_in(x1)
U3(x1, x2, x3, x4)  =  U3(x4)
append_in(x1, x2, x3)  =  append_in(x1, x2)
U6(x1, x2, x3, x4, x5)  =  U6(x5)
append_out(x1, x2, x3)  =  append_out(x3)
U4(x1, x2, x3, x4)  =  U4(x4)
last_in(x1, x2)  =  last_in(x2)
U5(x1, x2, x3, x4)  =  U5(x4)
last_out(x1, x2)  =  last_out
applast_out(x1, x2, x3)  =  applast_out
goal_out(x1, x2, x3)  =  goal_out
S2L_IN(x1, x2)  =  S2L_IN(x1)
U51(x1, x2, x3, x4)  =  U51(x4)
U31(x1, x2, x3, x4)  =  U31(x4)
LAST_IN(x1, x2)  =  LAST_IN(x2)
U41(x1, x2, x3, x4)  =  U41(x4)
APPLAST_IN(x1, x2, x3)  =  APPLAST_IN(x1)
APPEND_IN(x1, x2, x3)  =  APPEND_IN(x1, x2)
U21(x1, x2, x3, x4)  =  U21(x4)
U61(x1, x2, x3, x4, x5)  =  U61(x5)
U71(x1, x2, x3, x4)  =  U71(x4)
GOAL_IN(x1, x2, x3)  =  GOAL_IN(x1)
U11(x1, x2, x3, x4)  =  U11(x4)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 3 SCCs with 11 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

LAST_IN(X, .(H, T)) → LAST_IN(X, T)

The TRS R consists of the following rules:

goal_in(A, B, C) → U1(A, B, C, s2l_in(A, D))
s2l_in(0, []) → s2l_out(0, [])
s2l_in(s(X), .(Y, Xs)) → U7(X, Y, Xs, s2l_in(X, Xs))
U7(X, Y, Xs, s2l_out(X, Xs)) → s2l_out(s(X), .(Y, Xs))
U1(A, B, C, s2l_out(A, D)) → U2(A, B, C, applast_in(D, B, C))
applast_in(L, X, Last) → U3(L, X, Last, append_in(L, .(X, []), LX))
append_in(.(H, L1), L2, .(H, L3)) → U6(H, L1, L2, L3, append_in(L1, L2, L3))
append_in([], L, L) → append_out([], L, L)
U6(H, L1, L2, L3, append_out(L1, L2, L3)) → append_out(.(H, L1), L2, .(H, L3))
U3(L, X, Last, append_out(L, .(X, []), LX)) → U4(L, X, Last, last_in(Last, LX))
last_in(X, .(H, T)) → U5(X, H, T, last_in(X, T))
last_in(X, .(X, [])) → last_out(X, .(X, []))
U5(X, H, T, last_out(X, T)) → last_out(X, .(H, T))
U4(L, X, Last, last_out(Last, LX)) → applast_out(L, X, Last)
U2(A, B, C, applast_out(D, B, C)) → goal_out(A, B, C)

The argument filtering Pi contains the following mapping:
goal_in(x1, x2, x3)  =  goal_in(x1)
U1(x1, x2, x3, x4)  =  U1(x4)
s2l_in(x1, x2)  =  s2l_in(x1)
0  =  0
[]  =  []
s2l_out(x1, x2)  =  s2l_out(x2)
s(x1)  =  s(x1)
.(x1, x2)  =  .(x2)
U7(x1, x2, x3, x4)  =  U7(x4)
U2(x1, x2, x3, x4)  =  U2(x4)
applast_in(x1, x2, x3)  =  applast_in(x1)
U3(x1, x2, x3, x4)  =  U3(x4)
append_in(x1, x2, x3)  =  append_in(x1, x2)
U6(x1, x2, x3, x4, x5)  =  U6(x5)
append_out(x1, x2, x3)  =  append_out(x3)
U4(x1, x2, x3, x4)  =  U4(x4)
last_in(x1, x2)  =  last_in(x2)
U5(x1, x2, x3, x4)  =  U5(x4)
last_out(x1, x2)  =  last_out
applast_out(x1, x2, x3)  =  applast_out
goal_out(x1, x2, x3)  =  goal_out
LAST_IN(x1, x2)  =  LAST_IN(x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

LAST_IN(X, .(H, T)) → LAST_IN(X, T)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
LAST_IN(x1, x2)  =  LAST_IN(x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

LAST_IN(.(T)) → LAST_IN(T)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

APPEND_IN(.(H, L1), L2, .(H, L3)) → APPEND_IN(L1, L2, L3)

The TRS R consists of the following rules:

goal_in(A, B, C) → U1(A, B, C, s2l_in(A, D))
s2l_in(0, []) → s2l_out(0, [])
s2l_in(s(X), .(Y, Xs)) → U7(X, Y, Xs, s2l_in(X, Xs))
U7(X, Y, Xs, s2l_out(X, Xs)) → s2l_out(s(X), .(Y, Xs))
U1(A, B, C, s2l_out(A, D)) → U2(A, B, C, applast_in(D, B, C))
applast_in(L, X, Last) → U3(L, X, Last, append_in(L, .(X, []), LX))
append_in(.(H, L1), L2, .(H, L3)) → U6(H, L1, L2, L3, append_in(L1, L2, L3))
append_in([], L, L) → append_out([], L, L)
U6(H, L1, L2, L3, append_out(L1, L2, L3)) → append_out(.(H, L1), L2, .(H, L3))
U3(L, X, Last, append_out(L, .(X, []), LX)) → U4(L, X, Last, last_in(Last, LX))
last_in(X, .(H, T)) → U5(X, H, T, last_in(X, T))
last_in(X, .(X, [])) → last_out(X, .(X, []))
U5(X, H, T, last_out(X, T)) → last_out(X, .(H, T))
U4(L, X, Last, last_out(Last, LX)) → applast_out(L, X, Last)
U2(A, B, C, applast_out(D, B, C)) → goal_out(A, B, C)

The argument filtering Pi contains the following mapping:
goal_in(x1, x2, x3)  =  goal_in(x1)
U1(x1, x2, x3, x4)  =  U1(x4)
s2l_in(x1, x2)  =  s2l_in(x1)
0  =  0
[]  =  []
s2l_out(x1, x2)  =  s2l_out(x2)
s(x1)  =  s(x1)
.(x1, x2)  =  .(x2)
U7(x1, x2, x3, x4)  =  U7(x4)
U2(x1, x2, x3, x4)  =  U2(x4)
applast_in(x1, x2, x3)  =  applast_in(x1)
U3(x1, x2, x3, x4)  =  U3(x4)
append_in(x1, x2, x3)  =  append_in(x1, x2)
U6(x1, x2, x3, x4, x5)  =  U6(x5)
append_out(x1, x2, x3)  =  append_out(x3)
U4(x1, x2, x3, x4)  =  U4(x4)
last_in(x1, x2)  =  last_in(x2)
U5(x1, x2, x3, x4)  =  U5(x4)
last_out(x1, x2)  =  last_out
applast_out(x1, x2, x3)  =  applast_out
goal_out(x1, x2, x3)  =  goal_out
APPEND_IN(x1, x2, x3)  =  APPEND_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

APPEND_IN(.(H, L1), L2, .(H, L3)) → APPEND_IN(L1, L2, L3)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
APPEND_IN(x1, x2, x3)  =  APPEND_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

APPEND_IN(.(L1), L2) → APPEND_IN(L1, L2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

S2L_IN(s(X), .(Y, Xs)) → S2L_IN(X, Xs)

The TRS R consists of the following rules:

goal_in(A, B, C) → U1(A, B, C, s2l_in(A, D))
s2l_in(0, []) → s2l_out(0, [])
s2l_in(s(X), .(Y, Xs)) → U7(X, Y, Xs, s2l_in(X, Xs))
U7(X, Y, Xs, s2l_out(X, Xs)) → s2l_out(s(X), .(Y, Xs))
U1(A, B, C, s2l_out(A, D)) → U2(A, B, C, applast_in(D, B, C))
applast_in(L, X, Last) → U3(L, X, Last, append_in(L, .(X, []), LX))
append_in(.(H, L1), L2, .(H, L3)) → U6(H, L1, L2, L3, append_in(L1, L2, L3))
append_in([], L, L) → append_out([], L, L)
U6(H, L1, L2, L3, append_out(L1, L2, L3)) → append_out(.(H, L1), L2, .(H, L3))
U3(L, X, Last, append_out(L, .(X, []), LX)) → U4(L, X, Last, last_in(Last, LX))
last_in(X, .(H, T)) → U5(X, H, T, last_in(X, T))
last_in(X, .(X, [])) → last_out(X, .(X, []))
U5(X, H, T, last_out(X, T)) → last_out(X, .(H, T))
U4(L, X, Last, last_out(Last, LX)) → applast_out(L, X, Last)
U2(A, B, C, applast_out(D, B, C)) → goal_out(A, B, C)

The argument filtering Pi contains the following mapping:
goal_in(x1, x2, x3)  =  goal_in(x1)
U1(x1, x2, x3, x4)  =  U1(x4)
s2l_in(x1, x2)  =  s2l_in(x1)
0  =  0
[]  =  []
s2l_out(x1, x2)  =  s2l_out(x2)
s(x1)  =  s(x1)
.(x1, x2)  =  .(x2)
U7(x1, x2, x3, x4)  =  U7(x4)
U2(x1, x2, x3, x4)  =  U2(x4)
applast_in(x1, x2, x3)  =  applast_in(x1)
U3(x1, x2, x3, x4)  =  U3(x4)
append_in(x1, x2, x3)  =  append_in(x1, x2)
U6(x1, x2, x3, x4, x5)  =  U6(x5)
append_out(x1, x2, x3)  =  append_out(x3)
U4(x1, x2, x3, x4)  =  U4(x4)
last_in(x1, x2)  =  last_in(x2)
U5(x1, x2, x3, x4)  =  U5(x4)
last_out(x1, x2)  =  last_out
applast_out(x1, x2, x3)  =  applast_out
goal_out(x1, x2, x3)  =  goal_out
S2L_IN(x1, x2)  =  S2L_IN(x1)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

S2L_IN(s(X), .(Y, Xs)) → S2L_IN(X, Xs)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
.(x1, x2)  =  .(x2)
S2L_IN(x1, x2)  =  S2L_IN(x1)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

S2L_IN(s(X)) → S2L_IN(X)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: